
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Backend.Lib.EOperators</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Backend.Lib.EOperators" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Backend.Lib.EOperators</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.Ascii.html">Ascii</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.ZArith.ZArith.html">ZArith</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html">Qcert.Common.Brands.BrandRelation</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html">ErgoSpec.Backend.Model.ErgoBackendModel</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendRuntime.html">ErgoSpec.Backend.Model.ErgoBackendRuntime</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html">ErgoSpec.Backend.Lib.EData</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="EOperators">EOperators</a></span>(<span class="id">ergomodel</span>:<span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html#ErgoBackendModel">ErgoBackendModel</a></span>).<br/>
&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.ErgoData">ErgoData</a></span> := <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData">EData.EData</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#ergomodel">ergomodel</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Unary">Unary</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.op">op</a></span> : <span class="kwd">Set</span>  <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#unary_op">UnaryOperators.unary_op</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.t">t</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Unary.Double">Double</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opuminus">opuminus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatUnary">UnaryOperators.OpFloatUnary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#FloatNeg">UnaryOperators.FloatNeg</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opabs">opabs</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatUnary">UnaryOperators.OpFloatUnary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#FloatAbs">UnaryOperators.FloatAbs</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.oplog2">oplog2</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatUnary">UnaryOperators.OpFloatUnary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#FloatLog">UnaryOperators.FloatLog</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opsqrt">opsqrt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatUnary">UnaryOperators.OpFloatUnary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#FloatSqrt">UnaryOperators.FloatSqrt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opsum">opsum</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatSum">UnaryOperators.OpFloatSum</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opnummin">opnummin</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatBagMin">UnaryOperators.OpFloatBagMin</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opnummax">opnummax</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatBagMax">UnaryOperators.OpFloatBagMax</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.Double.opnummean">opnummean</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatMean">UnaryOperators.OpFloatMean</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.Double">Double</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opidentity">opidentity</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpIdentity">UnaryOperators.OpIdentity</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opneg">opneg</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpNeg">UnaryOperators.OpNeg</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.oprec">oprec</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRec">UnaryOperators.OpRec</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opdot">opdot</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDot">UnaryOperators.OpDot</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.oprecremove">oprecremove</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRecRemove">UnaryOperators.OpRecRemove</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.oprecproject">oprecproject</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRecProject">UnaryOperators.OpRecProject</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opbag">opbag</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpBag">UnaryOperators.OpBag</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opsingleton">opsingleton</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpSingleton">UnaryOperators.OpSingleton</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opflatten">opflatten</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFlatten">UnaryOperators.OpFlatten</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opdistinct">opdistinct</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDistinct">UnaryOperators.OpDistinct</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opcount">opcount</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpCount">UnaryOperators.OpCount</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.optostring">optostring</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpToString">UnaryOperators.OpToString</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opsubstring">opsubstring</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpSubstring">UnaryOperators.OpSubstring</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.oplike">oplike</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.Ascii.html#ascii">Ascii.ascii</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpLike">UnaryOperators.OpLike</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opleft">opleft</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpLeft">UnaryOperators.OpLeft</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opright">opright</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRight">UnaryOperators.OpRight</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opbrand">opbrand</a></span> <span class="id">b</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpBrand">UnaryOperators.OpBrand</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#b">b</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opunbrand">opunbrand</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpUnbrand">UnaryOperators.OpUnbrand</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.opcast">opcast</a></span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brands">BrandRelation.brands</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpCast">UnaryOperators.OpCast</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Unary.eval">eval</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">h</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brand_relation_t">BrandRelation.brand_relation_t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">uop</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#unary_op">UnaryOperators.unary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.ErgoData.data">ErgoData.data</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.ErgoData.data">ErgoData.data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperatorsSem.html#unary_op_eval">UnaryOperatorsSem.unary_op_eval</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#h">h</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#uop">uop</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#d">d</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Unary">Unary</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Binary">Binary</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.op">op</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#binary_op">BinaryOperators.binary_op</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.t">t</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Binary.Double">Double</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opplus">opplus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatPlus">BinaryOperators.FloatPlus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opminus">opminus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMinus">BinaryOperators.FloatMinus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opmult">opmult</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMult">BinaryOperators.FloatMult</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opmin">opmin</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMin">BinaryOperators.FloatMin</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opmax">opmax</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMax">BinaryOperators.FloatMax</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opdiv">opdiv</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatDiv">BinaryOperators.FloatDiv</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.oppow">oppow</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">BinaryOperators.OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatPow">BinaryOperators.FloatPow</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.oplt">oplt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">BinaryOperators.OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatLt">BinaryOperators.FloatLt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.ople">ople</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">BinaryOperators.OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatLe">BinaryOperators.FloatLe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opgt">opgt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">BinaryOperators.OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatGt">BinaryOperators.FloatGt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Double.opge">opge</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">BinaryOperators.OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatGe">BinaryOperators.FloatGe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.Double">Double</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Binary.Integer">Integer</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.opplusi">opplusi</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">BinaryOperators.OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatPlus">BinaryOperators.NatPlus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.opminusi">opminusi</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">BinaryOperators.OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatMinus">BinaryOperators.NatMinus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.opmulti">opmulti</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">BinaryOperators.OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatMult">BinaryOperators.NatMult</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.opdivi">opdivi</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">BinaryOperators.OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatDiv">BinaryOperators.NatDiv</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.oplti">oplti</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpLt">BinaryOperators.OpLt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.Integer.oplei">oplei</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpLe">BinaryOperators.OpLe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.Integer">Integer</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Module</span> <span class="id"><a name="EOperators.Binary.DateTime">DateTime</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdateplus">opdateplus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimePlus">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimePlus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdateminus">opdateminus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeMinus">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeMinus</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdatene">opdatene</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeNe">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeNe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdatelt">opdatelt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeLt">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeLt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdatele">opdatele</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeLe">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeLe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdategt">opdategt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGt">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdatege">opdatege</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGe">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGe</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdateintervaldays">opdateintervaldays</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalDays">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalDays</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.DateTime.opdateintervalseconds">opdateintervalseconds</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalSeconds">ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalSeconds</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.DateTime">DateTime</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opequal">opequal</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpEqual">BinaryOperators.OpEqual</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.oprecconcat">oprecconcat</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpRecConcat">BinaryOperators.OpRecConcat</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.oprecmerge">oprecmerge</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpRecMerge">BinaryOperators.OpRecMerge</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opand">opand</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpAnd">BinaryOperators.OpAnd</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opor">opor</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpOr">BinaryOperators.OpOr</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opbagunion">opbagunion</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpBagUnion">BinaryOperators.OpBagUnion</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opbagdiff">opbagdiff</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpBagDiff">BinaryOperators.OpBagDiff</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opbagmin">opbagmin</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpBagMin">BinaryOperators.OpBagMin</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opbagmax">opbagmax</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpBagMax">BinaryOperators.OpBagMax</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opcontains">opcontains</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpContains">BinaryOperators.OpContains</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.opstringconcat">opstringconcat</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary.op">op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpStringConcat">BinaryOperators.OpStringConcat</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EOperators.Binary.eval">eval</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">h</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brand_relation_t">BrandRelation.brand_relation_t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">bop</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#binary_op">BinaryOperators.binary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d1</span> <span class="id">d2</span>:<span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.ErgoData.data">ErgoData.data</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.ErgoData.data">ErgoData.data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperatorsSem.html#binary_op_eval">BinaryOperatorsSem.binary_op_eval</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#h">h</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#bop">bop</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#d2">d2</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators.Binary">Binary</a></span>.<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EOperators.html#EOperators">EOperators</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
